g:IAbMonoid, a, b, c:|g|. (a * (b * c)) = (b * (a * c))  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, IAbMonoid
Definitions	t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, x f y, IMonoid, IAbMonoid
Lemmas	iabmonoid wf, grp car wf, mon assoc, abmonoid comm, grp op wf